A, B, C, D:Type, h:(A(B + Top)), g:(B(C + Top)), f:(C(D + Top)).
f o g o h     = f o g   o h    A(D + Top) 

latex

ProofTree

Definitions	s = t, t  T, x:AB(x), x:A. B(x), f o g  , Type, left + right, Decision, inr x , Top, inl x , f(a), P  Q, S  T, b, outl(x), isl(x), if b then t else f fi , do-apply(f;x), can-apply(f;x)
Lemmas	ifthenelse wf, isl wf, outl wf, assert wf, member wf, top wf, p-compose wf